Zhaodan Kong

• 
  Formal Verification and Synthesis of Spatial Temporal Pattern for Networked Systems
  Zhaodan Kong
  Networked dynamical systems are increasingly used as models for a variety of processes ranging from robotic teams to collections of genetically engineered living cells. As the complexity of these systems increases, so does the range of emergent properties that they exhibit. In this short talk, I will propose a new logic called Spatial-Temporal Logic (SpaTeL) that is a unification of signal temporal logic (STL) and tree spatial superposition logic (TSSL). SpaTeL is capable of describing high-level spatial patterns that change over time. I will present a statistical model checking procedure that evaluates the probability with which a networked system satisfies a SpaTeL formula. I will also show a synthesis procedure that determines system parameters maximizing the average degree of satisfaction, a continuous measure that quantifies how strongly a system execution satisfies a given formula. Finally I will demonstrate our algorithms on some biological system models.